#include "rwtdb.h"
#include "base/aig.h"
#include "info/cktinfo.h"
#include "info/icut.h"

static void decode( unsigned short * dat , Arpreggio & arp  )
{
   arp.size = dat[0];
   arp.var  = dat[1];
   arp.score= dat[2];
   arp.npn.idx  = dat[3]>>1 ; arp.npn.sign = dat[3] & 1;
   arp.npn.in[0].decode( dat[4] >> 8 );
   arp.npn.in[1].decode( dat[4] & 0xFF );
   arp.npn.in[2].decode( dat[5] >> 8 );
   arp.npn.in[3].decode( dat[5] & 0xFF);
   arp.tapes = new AigNode [ dat[0] + 1 ]; 
   arp.tapes[ dat[0] ].key = 0 ;
}

bool RewriteDB::read_DB( const char * str )
{
   FILE * f = fopen( str , "rb" );
   if( f ==NULL ) 
   {
      printf("c wrong open %s \n", str); 
      printf("c YOU MUST RUN THE PROGRAM at \"synit_sat/\" with  \"synit_dat/dat/*\" \n");
      exit(1);
      return false;
   }
   
   fread( & _bucketSize , sizeof(unsigned) , 1 , f );
   _bucket = new AigLit[ _bucketSize ];
   fread( _mixers , sizeof(NPNPtr) , (1<<(1<<4)) , f );

   unsigned size;
   while( 1 )
   {
      fread( & size , sizeof( unsigned int ), 1 , f );
      if( feof( f ) ) break;

      _composition.push(); 
      _composition.last().growTo( size );
      for( unsigned int i = 0 ; i < size ; ++ i )
      { 
         Arpreggio & arp = _composition.last()[i];
         unsigned short dat[6];
         fread( dat , sizeof( unsigned short ) , 6 , f );
         decode( dat  , arp );
         fread( arp.tapes , sizeof(AigNode) , dat[0] , f );
      }
   }
   fclose(f);
   return true;
}
RewriteDB::~RewriteDB()
{
   for( unsigned i = 0 ; i < _composition.size() ; ++ i )
      for( unsigned j = 0 ; j < _composition[i].size() ; ++ j )
         delete [] _composition[i][j].tapes;
   delete [] _bucket;
}

///////////////////////////////////////////////////////////////////////////////
//                      Rewrite used function                                //
///////////////////////////////////////////////////////////////////////////////

void RewriteDB::put_bases( const Cut & c , unsigned s , NPNPtr mixer , const Arpreggio & arp )
{
   for( unsigned i = 0 ; i < s ; ++ i )
      _bucket[  arp.npn.in[i].permute ] = toAigLit( c[ mixer.in[i].permute ] , mixer.in[i].sign ^ arp.npn.in[i].sign );
}
unsigned RewriteDB::construct( const Arpreggio & arp , unsigned lim , unsigned & winner )
{
   AigNode * n = arp.tapes;
   AigLit  * b = _bucket + DBSIZE;
   unsigned cktsize = _ckt->size(); 
   for( ; n->key ; ++ n , ++b )
   {
      *b = _ckt->pseudo_createAND( _bucket[var(n->fanin[0])] ^ sign( n->fanin[0]) , _bucket[var(n->fanin[1])]^sign(n->fanin[1]) );
		if( var(*b) < cktsize ) *b = _info->eq( *b ); // improvement 
      if( var(*b) >= cktsize || (*_focnt)[ var(*b) ] == 0 ) lim -=1;
      if( lim == 0 || var(*b) == winner )return 0;
      //if( lim == 0 )return lim; FIX THE BUG
   }
   unsigned x = var( *(b-1) );
   if( x < cktsize &&  _info->eqIdx(x) != x ) return 0;
   winner = x;
   return lim;
}
// for each npn class constructing the target withing the limit 
unsigned RewriteDB::construct( fun_t f , const Cut & c , unsigned s , unsigned minpay , unsigned & winner )
{
   NPNPtr mixer = get_mixer( f );

   vec<Arpreggio> & arps = _composition[ mixer.idx ];

   unsigned size = _ckt->size();
   unsigned old_size = size;

   for( unsigned i = 0 ; i < arps.size() ; ++ i )
   {
      put_bases( c , s , mixer , arps[i] );

      unsigned pay = construct( arps[i] , minpay , winner );
      if( pay )
      { 
         if( old_size != size )
         {
            while( old_size != _ckt->size() )_ckt->pseudo_pop_back();
            _info->validation();
            construct( arps[i] , minpay , winner );
         }
         _info->validation();
         minpay -= pay; if(minpay==0)return minpay; 
         size = _ckt->size();
         arps[i].score+=1;
      }
      else while( size != _ckt->size() )_ckt->pseudo_pop_back();
   }
   _ckt->realize_and( old_size );
   return minpay;
}

